Document sources and false priority interfaces - #322

Source audit found two corrections needed before merge:

1. Challenges/BorceaBranden.lean should cite Borcea--Branden Theorem 1.2(b) for the real operator statement. Theorem 1.1 is the complex classification; its positive-symbol branch can also imply the result after complexification, but it is not the source theorem matching T : ℝ[X] →ₗ[ℝ] ℝ[X]. The nearby issue Retire the false homogeneous finiteSymbolBBStatement interface #314 audit already records Theorem 1.2(b).
2. Tactic/FiniteSymbolPF.lean says “See issue Prove the finite-symbol and homogenization stability backends #239”; the false homogeneous interface is tracked by Retire the false homogeneous finiteSymbolBBStatement interface #314.

The mathematical diagnosis and affine symbol formula in this PR are otherwise consistent with equations (1.1)--(1.2): G_T(z,w) = T((z+w)^κ).

A third citation correction is required. The finite Hurwitz-matrix Schur closure result is Garloff--Wagner Theorem 13 (pp. 807--808), not Theorem 1. Theorem 13 states that the Hadamard product of two nonsingular totally nonnegative finite n × n Hurwitz matrices is again a nonsingular totally nonnegative Hurwitz matrix. Please change both new “Theorem 1” references in Hadamard.lean and HurwitzMatrix.lean to Theorem 13. The primary PDF is now cached locally under DOI 10.1006/j.jmaa.1996.0348.

The Hoster--Stump source audit found a substantive blocker in the new comments. IsInterlacingSeq0Nonneg is not the paper's zero-aware interlacing-sequence predicate: Prec0 f g := f = 0 ∨ g = 0 ∨ Prec f g, so a zero entry can mask a non-real-rooted neighbor, and the predicate adds coefficient nonnegativity but not elementwise Splits. Consequently all four current interfaces are false. Explicit counterexamples already recorded on #316--#319 are [b,0], [0,b], [0,b,0], and [b], with b = 1+X+X^2.

Please do not say these declarations “deliberately ask for the corresponding zero-aware extension.” They currently ask for a weaker, invalid hypothesis. The source-faithful correction is to use the elementwise-real-rooted bundle introduced by PR #329 (IsInterlacingSeq0NonnegRealRooted) or add the equivalent explicit hypothesis. Lemma 2.3 itself uses the paper's zero-aware convention, but still requires every sequence member to be real-rooted.

Also note the printed indexing typo in Lemma 2.3(4): the displayed definition has 1 ≤ k ≤ n-ell, matching Lean's n-ell valid windows; the tuple label ending at r_{n-ell+1} is inconsistent.

For Proposition 2.5, the current gamma statement also needs nonnegative coefficients for gamma and delta (and a nonzero/exact-degree guard for the d=0 zero edge). PR #325 appears to own that correction; the source comment should describe the corrected hypotheses, not claim the old statement already encodes all of them.

The Jensen comment needs one further source correction. BidiagonalJensenPencilCertificate controls only J_{alpha,d}(t) + lambda * t * J_{beta,d}(t) for real lambda >= 0. Borcea--Branden Theorem 1.1 instead requires upper-half-plane stability of the genuine affine symbol

sum_{k=0}^d choose(d,k) * (alpha_k X^k + beta_k X^(k+1)) * Y^(d-k)

for independent complex X,Y in the upper half-plane. The one-sided pencil certificate does not currently imply that hypothesis. Garloff--Wagner Theorem 12 also assumes an oriented proper-position relation; it does not derive the needed orientation from the one-sided family.

Therefore the docstring should say this is an open PF-specific project conjecture/interface not stated in the cited papers. It should not say a source-faithful proof “must first identify the certificate” with affine-symbol stability, because no such identification is known and issue #240 contains a nested-root obstruction to the proposed orientation inference. The source-backed replacement is the affine-symbol wrapper with coefficient nonnegativity only for k <= d.

Pushed c21e11d8 as the scheduled cleanup pass. It incorporates the source-audit corrections without changing any declaration: Borcea--Branden Theorem 1.2(b) for the real interface, Garloff--Wagner Theorem 13 for finite Hurwitz matrices, issue #314 for the false homogeneous symbol, explicit legacy/false labels for the weak Hoster--Stump interfaces, the concrete Braun--Jal model requirement, and the Jensen pencil as an open project conjecture rather than a cited theorem. Seven files changed only in doc comments.

Coordination note: PR #325 now proves prec_gammaTransform_succ_iff in GammaRealRoots.lean, the reusable Hoster--Stump Proposition 2.5 backend needed for GammaAdjacentInterlacingTransferStatement. Please use that theorem when replacing the placeholder endpoint in Challenges/HosterStump.lean; PR #325 is deliberately not editing your owned challenge file.